k,m:, f:(int_seg(0; k)int_seg(0; m)), g:(int_seg(0; m)).
increasing(f; k)  increasing(g; m)  increasing(compose(g; f); k) 

latex

Definitions	suptype(S; T), subtype(S; T), t  T, compose(f; g), increasing(f; k), P  Q, x:A. B(x), False, A, A  B, P  Q, lelt(i; j; k), int_seg(i; j), , prop{i:l}, guard(T)
Lemmas	nat wf, increasing wf, int seg wf, le wf, increasing implies